00100	GIVEAX(SCINDUCTION,(∀ R)(∀ F)(∀ P)(SCORDERING R ∧ FεDOMAIN(R→→R)
00200	∧ Pε(DOMAIN R→TV) ∧AIW(P,R) ∧ β(P,UU)=T
00300	∧ (∀ X)(XεDOMAIN R ∧ β(P,X)=T ⊃ β(P,β(F,X))=T)
00400	⊃β(P,β(YCOMB(R),F))=T));
00500	
00600	GIVEAX(IGR1,(∀ R)(∀ P)(∀ Y)(SCORDERING R ∧ Pε(DOMAIN R → TV)
00700	∧ (∀ X)(Xε DOMAIN R ⊃ (β(P,X)= T ≡ ββ(X,R,Y)=T))
00800	⊃ AIW(P,R)));
     

00500	END;